Nuprl Lemma : reducible_wf
2,24
postcript
pdf
a
:
. reducible(
a
)
Prop
latex
Definitions
reducible(
a
)
,
x
:
A
.
B
(
x
)
,
P
&
Q
,
A
,
a
~
b
,
x
:
A
.
B
(
x
)
,
,
Prop
,
t
T
Lemmas
assoced
wf
,
not
wf
,
int
nzero
wf
origin
a:
. reducible(a) 
Prop a:. reducible(a) Prop 
x:A. B(x)
Ax:A. B(x)
T